2020-05-15 12:53:2 (GMT)
This is one very interesting and extremely hard problem:
( ! [Xp: ( $i > $i ) > $o] :
( ( ( Xp @ f )
& ! [Xj: $i > $i] :
( ( Xp @ Xj )
=> ( Xp
@ ^ [Xx: $i] :
( f @ ( Xj @ Xx ) ) ) ) )
=> ( Xp @ g ) )
=> ( ( ^ [Xx: $i] :
( f @ ( g @ Xx ) ) )
= ( ^ [Xx: $i] :
( g @ ( f @ Xx ) ) ) ) )).
2020-05-15 12:54:24 (GMT)
It can be solved if is instantiated with
2020-05-15 12:56:9 (GMT)
With current inference rules there is no way we can come to this term efficiently..
The closes thing we can do is primitive enumeration with
2020-05-15 12:56:30 (GMT)
and refine this further, which is just horrible.
2020-05-15 12:57:31 (GMT)
So, @Alexander Bentkamp : Is there anything in your full HO calculus that treats this efficiently (term that we need for instantiation cannot be obtained by unification as far as I can see)
@Ahmed B : How does Vampire fare with this problem
2020-05-15 13:17:6 (GMT)
For this problem it would be nice to use the Ganzinger and Stuber approach of having only positive literals and encoding negative literals as (s ≈ t) ≈ ⊥. If we do that, we get the clause (λx. f (g x) ≈ λx. g (f x)) ≈ ⊥, which could be used to obtain the right instantiation Xp := λ g. λx. f (g x) ≈ λx. g (f x) by unification.
2020-05-15 13:41:58 (GMT)
But with our current approach where we have proper negative literals I think primitive enumeration is necessary to come up with ≈. But is that really that bad? We've just learned that this kind of guessing is what Satallax does primarily :-)
2020-05-15 14:11:10 (GMT)
It seems to be extremely bad :frown:
2020-05-15 14:12:29 (GMT)
Primitive enumeration comes up with and then to get a correct term I am not 100% sure where you need to paramodulate
2020-05-15 14:13:10 (GMT)
But the whole premise is full of applied variables and I think taht the problem is just too explosive
2020-05-15 14:52:8 (GMT)
Here is how it could work:
λx. f (g x) ≉ λx. g (f x) and (2) P g ≈ ⊤ ⋁ (P f ∧ ∀J. P J → P (λx. f (J x))) ≈ ⊥F g ≈ G g ⋁ (F f ≈ G f ∧ ∀J. F J ≈ G J → F (λx. f (J x)) ≈ G (λx. f (J x))) ≈ ⊥G g ≉ λx. g (f x) ⋁ (λx. f (f x) ≈ G f ∧ ∀J. λx. f (J x) ≈ G J → λx. f (f (J x)) ≈ G (λx. f (J x))) ≈ ⊥(λx. f (f x) ≈ λx. f (f x) ∧ ∀J. λx. f (J x) ≈ λx. J (f x) → λx. f (f (J x)) ≈ λx. f (J (f x))) ≈ ⊥λx. f (sk x) ≈ λx. sk (f x) and λx. f (f (sk x)) ≉ λx. f (sk (f x))2020-05-15 14:52:28 (GMT)
But of course it's hard to find this proof automatically :-)
2020-05-15 15:25:13 (GMT)
Petar Vukmirovic said:
So, Alexander Bentkamp : Is there anything in your full HO calculus that treats this efficiently (term that we need for instantiation cannot be obtained by unification as far as I can see)
Ahmed B : How does Vampire fare with this problem
Vampire can't solve it. Neither the current version nor the previous version based on combinatory unification.
2020-05-15 17:4:58 (GMT)
Alexander Bentkamp said:
But of course it's hard to find this proof automatically :-)
I have tried hundreds of configurations and nothing works... I think the reason satallax finds the proof is that its instantiation is not so step-by-step with many explosive steps in between.
It just instantiates with the right term and then everything just aligns...
2020-05-15 17:7:40 (GMT)
The question is also, at what point do you stop? :)
2020-05-16 4:29:2 (GMT)
As I suspected, this is a TPS problem. These are those I had in mind when I wrote point 2 below (on the Matryoshka web page and in the grant proposal):
"Native higher-order automated reasoning has been researched since the late 1960s. However, this work has not produced a viable alternative to the Sledgehammer-style HO-to-FO translation. We see two reasons for this:
Higher-order reasoning has not yet assimilated the most successful first-order methods, namely superposition and SMT.
The existing provers are designed for small and tricky higher-order problems, whereas typical proof goals are only mildly higher-order but large.
Moreover, these provers do not support polymorphism, which is needed to reason about parameterized theories, and they usually fail to discover even trivial proofs by induction."
It is absolutely great that you look at each of those problems in detail, because they can give you ideas that may apply on more realistic problems. But I wouldn't worry or even be surprised if Satallax solves these. Satallax was developed to have enough modes to handle everything TPS could handle, basically. It's no coincidence it thrives on such problems. And TPS was a connection/mating prover and could do all these examples with the right mode; yet it was mostly useless as an ATP, because, as Chad pointed out jokingly, TPS probably never could prove a problem in which two or more unnecessary axioms are present. It's a very different ball game than what Matryoshka set out to achieve.
2020-05-16 4:33:13 (GMT)
If you're worried about the competition, it's also possible to flood TPTP with realistic sledgehammer problems :-)
2020-05-16 8:6:36 (GMT)
I tried, but Geoff turned down most of them.
2020-05-16 8:7:19 (GMT)
I should try again.
2020-05-16 16:8:29 (GMT)
Surprising, why would he reject them?
2020-05-16 18:7:59 (GMT)
Too many similar problems with unknown status.
2020-05-16 21:12:45 (GMT)
Are they unknown if they've been proven in Isabelle? Real question.
Also it seems like that's how you make progress! You need new problems that are hard…
2020-05-17 12:20:12 (GMT)
I'll take all those that at least one prover solves. I'll write to Geoff tomorrow.
2020-05-17 12:20:36 (GMT)
Due to the lemma selector and monomorphizer, there are no provability guarantees.
2020-05-18 13:23:15 (GMT)
Ah, getting more modern encodings of other problems from Mizar would also be cool. I imagine that even THF0 would be super cool (or does it just require TFF0?).
2020-05-18 13:57:21 (GMT)
Mizar is FOL + Set theory, right? Maybe we should work on superposition for set theory then :-)
2020-05-18 14:18:13 (GMT)
I think set theory's alternative name is "lambdas that return bool" :joy: